A, B:Type, eq1:EqDecider(A), eq2:EqDecider(B), L:((:A  B) List).
no_repeats(A;fpf-domain(fpf(L)))
& (a:A. (a  fpf-domain(fpf(L)))  (b:B. (<a, b>  L)))
& adom(fpf(L)). l=fpf(L)(a)   no_repeats(B;l) & (b:B. (b  l)  (<a, b>  L)) 

latex

Definitions

A c B, P & Q, t  T, x:A. B(x), EqDecider(T), x. t(x), fpf-domain(f), fpf(L), t.1, map(f;as), , (x  l), x:A. B(x), P  Q, P  Q, remove-repeats(eq;L), P  Q, t.2, True, T, no_repeats(T;l), Top, a:A fp B(a), x  dom(f), b, xdom(f). v=f(x)   P(x;v), f(x), insert(a;L), eqof(d), if b then t else f fi , reduce(f;k;as), A, b, , Unit, False, P  Q, , {T}

Lemmas

cons member, or functionality wrt iff, not functionality wrt iff, deq property, member-insert, false wf, nil member, no repeats nil, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, no repeats-insert, reduce wf, ifthenelse wf, eqof wf, insert wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, pairs-fpf wf, squash wf, true wf, all functionality wrt iff, iff functionality wrt iff, member map, iff wf, remove-repeats wf, pi2 wf, l member wf, remove-repeats property, map wf, pi1 wf, deq wf